Nuprl Lemma : grp_inverse
13,42
postcript
pdf
g
:IGroup,
a
:|
g
|. (
a
* (~(
a
))) = e
|
g
| & ((~(
a
)) *
a
) = e
|
g
|
latex
Up
groups
1
Definitions of Statement
IGroup
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
IGroup
,
Inverse(
T
;
op
;
id
;
inv
)
Lemmas
igrp
wf
,
igrp
properties
origin
g:IGroup, a:|g|. (a * (~(a))) = e 
|g| & ((~(a)) * a) = e |g| g:IGroup, a:|g|. (a * (~(a))) = e |g| & ((~(a)) * a) = e |g| Tx:A. B(x)